package interfaces;
import java.util.Date;
import java.util.List;

import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

@Init({"getCodigo() >= 0 && getCodigo() <= Integer.MAX_VALUE && getNombreCliente() != null && getDescripcion() != null && getEmailCliente() != null && getEmailCliente().matches(\"^[a-zA-Z0-9_-]{2,}\\.[a-zA-Z0-9_-]{2,}@[a-zA-Z0-9_-]{2,}\\.[a-zA-Z]{2,4}(\\.[a-zA-Z]{2,4})?\") && getCodigoProducto() >= 0 && getCodigoProducto() <= Integer.MAX_VALUE && getProcesamientoSeleccionado() != null && getFechaApertura() != null "})
@Inv({""}) 

public interface IIncidencia {
	@Query
	public int getCodigo();
	@Query
	public String getNombreCliente();
	@Query
	public String getEmailCliente();
	@Query
	public String getDescripcion();
	@Query
	public int getCodigoProducto();
	@Query
	public int getProcesamientoSelecionado();
	@Query
	public List<Integer> getIncidenciasRelacionadas();
	@Query
	public boolean getEsAbierta();
	@Query
	public Date getFechaApertura();
	@Query
	public boolean getEstaAsignada();
	
	@Pre ({"codigoNuevo >= 0 && codigoNuevo <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos ({"getCodigo() == codigoNuevo && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setCodigo(int codigoNuevo);
	@Pre ({"nombreNuevo != null #NullPointerException"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(nombreNuevo) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre	&& getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setNombreCliente(String nombreNuevo);
	@Pre ({"emailNuevo != null #NullPointerException", "emailNuevo.matches(\"^[a-zA-Z0-9_-]{2,}\\.[a-zA-Z0-9_-]{2,}@[a-zA-Z0-9_-]{2,}\\.[a-zA-Z]{2,4}(\\.[a-zA-Z]{2,4})?\")"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(nuevoEmail) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre	&& getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setEmailCliente(String emailNuevo);
	@Pre ({"descripcionNueva != null"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(descripcionNueva) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setDescripcion(String descripcionNueva);
	@Pre ({"codigoProcNuevo => 0 && codigoProcNuevo <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == codigoProcNuevo && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setCodigoProducto(int codigoProcNuevo);
	@Pre ({"procesamientoNuevo != null #NullPointerException"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == procesamientoNuevo && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setProcesamientoSelecionado(int procesamientoNuevo);
	@Pre ({"incidenciasNuevas != null #NullPointerException", "!incidenciasNuevas.isEmpty()"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == incidenciasNuevas && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setIncidenciasRelacionadas(List<Integer> incidenciasNuevas);
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == abiertaNueva && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setEsAbierta(boolean abiertaNueva);
	@Pre ({"fechaNueva != null #NullPointerException"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == fechaNueva	&& getEstaAsignada() == getEstaAsignada()@pre"})
	public void setFechaApertura(Date fechaNueva);
	@Pre ({"!getEstaAsignada()"})
	@Pos ({"getCodigo() == getCodigo()@pre && getNombreCliente().equals(getNombreCliente()@pre) && getEmailCliente().equals(getEmailCliente()@pre) && getDescripcion().equals(getDescripcion()@pre) && getCodigoProducto() == getCodigoProducto()@pre && getProcesamientoSeleccionado() == getProcesamientoSeleccionado()@pre && getIncidenciasRelacionadas() == getIncidenciasRelacionadas()@pre && getEsAbierta() == getEsAbierta()@pre && getFechaApertura() == getFechaApertura()@pre	&& getEstaAsignada() == asignacionNueva"})
	public void setEstaAsignada(boolean asignacionNueva);
}
